COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.<<to raproachment???>>
C00017 ENDMK
C⊗;
.<<to raproachment???>>
We can give some insight into the mathematical properites of
%3label%1; we continue our discussion of {yonss(P85)}.
As before, we take our clues from the behavior of %3eval%* and %3apply%*.
In any environment %9D%4a%1 should map %3label[f;g]%* in such a way that the 
denotation of %3f%* is synonymous with that of %3g%*.
That is, %df%* is a mapping satisfying the equation 
%df(t%4i%*,#...,#t%4n%*)#=#%dg(t%4i%*,#...,#t%4n%*)%1.
So:

.BEGIN CENTERIT;FILL;TURN ON "#";
←%9D%4a%f(%3label[%af%1;%ag%1]%f)%d(l)%1#=#%9D%4a%f(%ag%f)%d(l)%1.
.END

This will suffice for our current λ-definitions; we need not modify %dl%*
since the name %3f%* will never be used within the evaluation of 
an expression involving %3g%*.

.BEGIN TURN ON "#";
We must be a bit careful.
Our treatment of evaluation of free
variables in LISP (on {yon(P93)} and in {yonss(P77)}) shows that free
variables in a function are to be evaluated when the function is %2activated%*
rather than when
 the function is defined. Thus a λ-definition generally
requires an environment in which to evaluate its free variables.
So its denotation 
should be a mapping like: %denv%*#→#%d[%aS%8n%d#→#%aS%d]%1 rather than
simply %d[%aS%8n%d#→#%aS%d]%1. This is consistent with our understanding of the
meaning of λ-notation.
It is what %3function%* was attempting to 
describe. 
What we previously have called an ⊗→open function↔← is  of the
form: %d[%aS%8n%d#→#%aS%d]%1.

.END
 This view of λ-notation must change our conception on %denv%* as well.
Given a name for a function in an environment we can expect to receive
a mapping from %denv%* to an element of %aFn%*. That is, for such names:

.BEGIN CENTERIT;
←%denv %1is the set of functions: %aId%d → [%denv → %aFn%d]%1.
.END

A modification of our handling of %3label%* seems to describe the case 
for recursion:

.BEGIN CENTERIT;FILL;TURN ON "#";
←%9D%4a%f(%3label[%af%1;%ag%1]%f)%d(l)%1#=#%9D%4a%f(%ag%f)%d(l#:#<f,%9D%4a%f(%ag%f)%d>)%1.
.END

Interpreting this equation operationally, it says: when we apply a %3label%*
expression in an environment it is the same as applying the body of the definition
in an environment modified to  associate the name with its definition.
This is analogous to what the LISP %3apply%* function will do.
Since this interpretation of %3label%* is inadequate in
general contexts,
we should  look further for a general reading of %3label%*. Our hint
comes from our interpretation of "<=" as an equality. Recall:

.BEGIN CENTER;SELECT 3;TURN OFF "←";

fact ← %1a solution to the equation:%* f = λ[[x][x=0 → 1; %et%3 → *[x;f[x-1]]]].
.END
What we need is a representation of an "equation-solver" which will
take such an equation and will return  a function
which satisfies that equation. In particular we would like the %2best%* 
solution in the sense that it imposes the minimal structure on the function⊗↓Like 
a free group satisfies the group axioms, but imposes no other
requirements.←.
This request for minimality translates to finding the function which
satisfies the equation, but is least-defined on other elements of the
domain. This discussion of "least" brings in the recent work of D. Scott
and  the intuition behind
this study  again illuminates the distinction
between mathematical meaning (denotational) and manipulative meaning (operational).

Consider the following LISP definition:

.BEGIN CENTER;SELECT 3;

f <= λ[[n][n=0 → 0; %et%3 → f[n-1] + 2*n -1]]
.END

.BEGIN TURN ON "#";
When we are asked what this function is doing, most of us would proceed
operationally; that is, we would begin computing %3f[n]%* for different
values of %3n%* --what#is#%3f[0]?%*,
 what is %3f[1]%1,#...#. It is profitable to look at this process differently:
what we are doing is looking  at a %2sequence%* of functions,
call them %df%4i%1's .
.END

.BEGIN TABIT3(10,16,44);SELECT d;GROUP;TURN OFF "{","}";

\f%40%1 =\%d{<0,%9B%*>,<1,%9B%*>, ... }\%1when we begin, we know nothing.
\%df%41%1 =\%d{<0,0>,<1,%9B%*>, ... }\%1now we know one pair.
\%df%42%1 =\%d{<0,0>,<1,1>, ... }\%1now two
\%df%43%1 =\%d{<0,0>,<1,1>,<2,4>, ... }\%1now three

\ ...\           ...          ...\%dEureka!!
.END

When or if, we realize that the LISP function is
"really" (denotationally)  the "squaring function",
then we have moved from pragmatics to semantics.
 The process of discovering
the denotation  may be likened to  a limiting process which creates 
converges to a function satisfying the LISP definition. 
.GROUP;
That is:

.BEGIN CENTER;SELECT d;

%9λ%d((n)n%82%d)%1 = %1limit of the %d f%4i%1's;
.END
where %df%4i%1 may also be characterised as:

.BEGIN TABIT1(12);SELECT D;group;

\ %1|%d n%82%1 if %d0%c≤%dn%c≤%di
f%4i%d(n)%1 =\<
\ | %9B%1 if %di%c<%dn

.END
.APART

We may think of our "equation-solver" as proceeding in such a manner.
As with simpler equations, there may be several solutions. For example,
we have seen that a function, %3g%1, defined to be %3n!%1 for %3n%a≥%30%1 and
%30%1 for %3n%a<%30%1 also satisfies the LISP definition of %3fact%1.
The expected solution for %3fact%1 is undefined for %3n%a<%30%1, and is
therefore  "less defined" than %3g%1. We would like our equation solver
to produce a minimal solution, if possible.
Such an equation solver
%2does%* exist; it is called the %2⊗→fixed-point operator↔←%*. It is 
designated here by %dY%*. To comprehend %dY%1 we generalize from the previous 
example.

.GROUP;
In terms of our example we want a solution to %df = %9t%d(f)%1, where:

.BEGIN CENTER;
%9t%d(g) = %9λ%d((n) if(n=0, 0, g(n-1)+2*n-1))%1,
.END

Our previous discussion leads us to believe that
%9λ%d((n)n%82%d) %1for %dn %c≥%d0%1 is the desired solution.
.APART

.BEGIN TURN ON "#";

How does this discussion relate to the sequence of functions %df%4i%1?
First, it's important to keep the domains of our various mapping in mind:
%df%*#%9ε%*#Fn and %9t%* is a functional in %aFn%1#→#%aFn%1.
Let's look at the behavior of %9t%* for various 
arguments. The simplest function is the totally undefined function, %9B%*#⊗↓We 
perhaps should subscript %9B%* to distinguish it from previous %9B%*'s.←.


.GROUP;
.BEGIN CENTER;
%9t%d(%9B%d) = %9λ%d((n) if(n=0, 0, %9B%*(n-1)+2*n-1))%1,
.END
but this says %9t%d(%9B%*)%1 is just %df%41%1.
Similarly,
.BEGIN CENTER;
%9t%d(%9t%d(%9B%*))#=#%9λ%d((n) if(n=0, 0, f%41%*(n-1)+2*n-1))%1,
.END
is just %df%42%1.
Writing %9t%8i%1 for the composition of %9t%1...%9t%1, i times, ⊗↓Define
%9t%80%1 to be the the totally undefined function, %9B%1.← we can say
.BEGIN CENTER;GROUP;

%df%4i%* = %9t%8i%d(%9B%*)%1  or,

%9λ%d((n)n%82%*)%1 = lim%4i → ∞%9t%8i%d(%9B%d)%1.
.END
.APART

.GROUP;
Or in general the fixed-point of an equation %df = %9t%*(f)%1 satisfies the
relation:

.BEGIN CENTER;

%dY(%9t%*) = lim%4i→∞%9t%8n%d(%9B%d).%1
.END
In summary, %dY%* is a mapping: %d[[%aFn%* → %aFn%*] → %aFn%*]%1
such that if %9t%*#%9ε%d#[%aFn%*#→#%aFn%*]%1 and %df%*#=#%9t%d(f)%1, then
%9t%d(Y(%9t%*))%1#=#%dY(%9t%*)%1. Comapre this relationship to that attributed to
the %dY%1 expression of the %9λ%1-calculus on {yon(P271)}.
.END
.APART

.GROUP;

So the search for denotations for %3label%* might be better served by:

.BEGIN CENTERIT;FILL;TURN ON "#";
←%9D%4a%f(%3label[%af%1;%ag%1]%f)%d(l)%1#=
#%dY(%9λ%d(h)%9D%4a%f(%ag%f)%d(l%1#:#%d<f,h>))%1.
.END
.APART


The characterizations are %2not%* the same. Examination of the
behavior of %9D%4e%f(%3label[car;car][(A#B)]%f)%1 will exhibit a discrepancy.
Which characterization of %3label[f;g]%* is "better"?
The first denotation parallels the behavior of %3eval%* and %3apply%*, applying
%3g%* in a %denv%* modified by  the pair %d<f,g>%*.
The later fix-point characterization says %3label[f;g]%* is a particular
solution the the equation %df#=#g%*. As we have seen, the "meaning" of %3label%*
is better served by this fix-point interpretation. The crucial questions, however,
are: first, are these two  denotations different? 
And which, if either, interpretation is %2correct%*? 
That is, which
characterization has the same %2effect%* as %3eval%* and %3apply%*?

The general question of the correctness of the denotational semantics which we
are developing is the subject of much of M. Gordon's thesis.
The informality of the current discussion can be replaced with precision.
The natural ordering
of "less defined" exemplified by the sequence of %df%4i%1's: %df%4i%1 is less
defined (or approximates) %df%4j%1, j%c≥%1i, imposes a structure on our domain of functions.
In fact, a structure can be naturally superimposed on all of our domains.
If we require that some additional simple properties hold on our domains, then
the intuitions of this section can be justified mathematically.